<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Bib: Bibliography</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: Logical Foundations</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>


<div class="doc">

<div class="paragraph"> </div>

<a name="lab388"></a><h1 class="section">Resources cited in this volume</h1>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<a target="Bertot 2004"><span class="inlineref"><b>[Bertot 2004]</b></span></a> Interactive Theorem Proving and Program Development:
  Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and
  Pierre Casteran.  Springer-Verlag, 2004.
  <a href="http://tinyurl.com/z3o7nqu"><span class="inlineref">http://tinyurl.com/z3o7nqu</span></a>

<div class="paragraph"> </div>

<a target="Chlipala 2013"><span class="inlineref"><b>[Chlipala 2013]</b></span></a> Certified Programming with Dependent Types, by
  Adam Chlipala.  MIT Press.  2013.  <a href="http://tinyurl.com/zqdnyg2"><span class="inlineref">http://tinyurl.com/zqdnyg2</span></a>

<div class="paragraph"> </div>

<a target="Lipovaca 2011"><span class="inlineref"><b>[Lipovaca 2011]</b></span></a> Learn You a Haskell for Great Good! A Beginner's
  Guide, by Miran Lipovaca, No Starch Press, April 2011.
  <a href="http://learnyouahaskell.com"><span class="inlineref">http://learnyouahaskell.com</span></a>

<div class="paragraph"> </div>

<a target="O'Sullivan 2008"><span class="inlineref"><b>[O'Sullivan 2008]</b></span></a> Bryan O'Sullivan, John Goerzen, and Don Stewart:
  Real world Haskell - code you can believe in. O'Reilly
  2008. <a href="http://book.realworldhaskell.org"><span class="inlineref">http://book.realworldhaskell.org</span></a>

<div class="paragraph"> </div>

<a target="Pugh 1991"><span class="inlineref"><b>[Pugh 1991]</b></span></a> Pugh, William. "The Omega test: a fast and practical
  integer programming algorithm for dependence analysis." Proceedings
  of the 1991 ACM/IEEE conference on Supercomputing. ACM, 1991.
  <a href="http://dl.acm.org/citation.cfm?id=125848"><span class="inlineref">http://dl.acm.org/citation.cfm?id=125848</span></a>

<div class="paragraph"> </div>

<a target="Wadler 2015"><span class="inlineref"><b>[Wadler 2015]</b></span></a> Philip Wadler. "Propositions as types."
  Communications of the ACM 58, no. 12 (2015): 75-84.
  <a href="http://dl.acm.org/citation.cfm?id=2699407"><span class="inlineref">http://dl.acm.org/citation.cfm?id=2699407</span></a>

<div class="paragraph"> </div>


</div>
</div>



</div>

</body>
</html>